Left Termination of the query pattern q_in_2(g, g) w.r.t. the given Prolog program could successfully be proven:



↳ Prolog
  ↳ PrologToPiTRSProof

Clauses:

e(a, b).
q(X, Y) :- e(X, Y).
q(X, f(f(X))) :- ','(p(X, f(f(X))), q(X, f(X))).
q(X, f(f(Y))) :- p(X, f(Y)).
p(X, Y) :- e(X, Y).
p(X, f(Y)) :- ','(r(X, f(Y)), p(X, Y)).
r(X, Y) :- e(X, Y).
r(X, f(Y)) :- ','(q(X, Y), r(X, Y)).
r(f(X), f(X)) :- t(f(X), f(X)).
t(X, Y) :- e(X, Y).
t(f(X), f(Y)) :- ','(q(f(X), f(Y)), t(X, Y)).

Queries:

q(g,g).

We use the technique of [30].Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

q_in(X, f(f(Y))) → U4(X, Y, p_in(X, f(Y)))
p_in(X, f(Y)) → U6(X, Y, r_in(X, f(Y)))
r_in(f(X), f(X)) → U11(X, t_in(f(X), f(X)))
t_in(f(X), f(Y)) → U13(X, Y, q_in(f(X), f(Y)))
q_in(X, f(f(X))) → U2(X, p_in(X, f(f(X))))
p_in(X, Y) → U5(X, Y, e_in(X, Y))
e_in(a, b) → e_out(a, b)
U5(X, Y, e_out(X, Y)) → p_out(X, Y)
U2(X, p_out(X, f(f(X)))) → U3(X, q_in(X, f(X)))
q_in(X, Y) → U1(X, Y, e_in(X, Y))
U1(X, Y, e_out(X, Y)) → q_out(X, Y)
U3(X, q_out(X, f(X))) → q_out(X, f(f(X)))
U13(X, Y, q_out(f(X), f(Y))) → U14(X, Y, t_in(X, Y))
t_in(X, Y) → U12(X, Y, e_in(X, Y))
U12(X, Y, e_out(X, Y)) → t_out(X, Y)
U14(X, Y, t_out(X, Y)) → t_out(f(X), f(Y))
U11(X, t_out(f(X), f(X))) → r_out(f(X), f(X))
r_in(X, f(Y)) → U9(X, Y, q_in(X, Y))
U9(X, Y, q_out(X, Y)) → U10(X, Y, r_in(X, Y))
r_in(X, Y) → U8(X, Y, e_in(X, Y))
U8(X, Y, e_out(X, Y)) → r_out(X, Y)
U10(X, Y, r_out(X, Y)) → r_out(X, f(Y))
U6(X, Y, r_out(X, f(Y))) → U7(X, Y, p_in(X, Y))
U7(X, Y, p_out(X, Y)) → p_out(X, f(Y))
U4(X, Y, p_out(X, f(Y))) → q_out(X, f(f(Y)))

The argument filtering Pi contains the following mapping:
q_in(x1, x2)  =  q_in(x1, x2)
f(x1)  =  f(x1)
U4(x1, x2, x3)  =  U4(x3)
p_in(x1, x2)  =  p_in(x1, x2)
U6(x1, x2, x3)  =  U6(x1, x2, x3)
r_in(x1, x2)  =  r_in(x1, x2)
U11(x1, x2)  =  U11(x2)
t_in(x1, x2)  =  t_in(x1, x2)
U13(x1, x2, x3)  =  U13(x1, x2, x3)
U2(x1, x2)  =  U2(x1, x2)
U5(x1, x2, x3)  =  U5(x3)
e_in(x1, x2)  =  e_in(x1, x2)
a  =  a
b  =  b
e_out(x1, x2)  =  e_out
p_out(x1, x2)  =  p_out
U3(x1, x2)  =  U3(x2)
U1(x1, x2, x3)  =  U1(x3)
q_out(x1, x2)  =  q_out
U14(x1, x2, x3)  =  U14(x3)
U12(x1, x2, x3)  =  U12(x3)
t_out(x1, x2)  =  t_out
r_out(x1, x2)  =  r_out
U9(x1, x2, x3)  =  U9(x1, x2, x3)
U10(x1, x2, x3)  =  U10(x3)
U8(x1, x2, x3)  =  U8(x3)
U7(x1, x2, x3)  =  U7(x3)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

q_in(X, f(f(Y))) → U4(X, Y, p_in(X, f(Y)))
p_in(X, f(Y)) → U6(X, Y, r_in(X, f(Y)))
r_in(f(X), f(X)) → U11(X, t_in(f(X), f(X)))
t_in(f(X), f(Y)) → U13(X, Y, q_in(f(X), f(Y)))
q_in(X, f(f(X))) → U2(X, p_in(X, f(f(X))))
p_in(X, Y) → U5(X, Y, e_in(X, Y))
e_in(a, b) → e_out(a, b)
U5(X, Y, e_out(X, Y)) → p_out(X, Y)
U2(X, p_out(X, f(f(X)))) → U3(X, q_in(X, f(X)))
q_in(X, Y) → U1(X, Y, e_in(X, Y))
U1(X, Y, e_out(X, Y)) → q_out(X, Y)
U3(X, q_out(X, f(X))) → q_out(X, f(f(X)))
U13(X, Y, q_out(f(X), f(Y))) → U14(X, Y, t_in(X, Y))
t_in(X, Y) → U12(X, Y, e_in(X, Y))
U12(X, Y, e_out(X, Y)) → t_out(X, Y)
U14(X, Y, t_out(X, Y)) → t_out(f(X), f(Y))
U11(X, t_out(f(X), f(X))) → r_out(f(X), f(X))
r_in(X, f(Y)) → U9(X, Y, q_in(X, Y))
U9(X, Y, q_out(X, Y)) → U10(X, Y, r_in(X, Y))
r_in(X, Y) → U8(X, Y, e_in(X, Y))
U8(X, Y, e_out(X, Y)) → r_out(X, Y)
U10(X, Y, r_out(X, Y)) → r_out(X, f(Y))
U6(X, Y, r_out(X, f(Y))) → U7(X, Y, p_in(X, Y))
U7(X, Y, p_out(X, Y)) → p_out(X, f(Y))
U4(X, Y, p_out(X, f(Y))) → q_out(X, f(f(Y)))

The argument filtering Pi contains the following mapping:
q_in(x1, x2)  =  q_in(x1, x2)
f(x1)  =  f(x1)
U4(x1, x2, x3)  =  U4(x3)
p_in(x1, x2)  =  p_in(x1, x2)
U6(x1, x2, x3)  =  U6(x1, x2, x3)
r_in(x1, x2)  =  r_in(x1, x2)
U11(x1, x2)  =  U11(x2)
t_in(x1, x2)  =  t_in(x1, x2)
U13(x1, x2, x3)  =  U13(x1, x2, x3)
U2(x1, x2)  =  U2(x1, x2)
U5(x1, x2, x3)  =  U5(x3)
e_in(x1, x2)  =  e_in(x1, x2)
a  =  a
b  =  b
e_out(x1, x2)  =  e_out
p_out(x1, x2)  =  p_out
U3(x1, x2)  =  U3(x2)
U1(x1, x2, x3)  =  U1(x3)
q_out(x1, x2)  =  q_out
U14(x1, x2, x3)  =  U14(x3)
U12(x1, x2, x3)  =  U12(x3)
t_out(x1, x2)  =  t_out
r_out(x1, x2)  =  r_out
U9(x1, x2, x3)  =  U9(x1, x2, x3)
U10(x1, x2, x3)  =  U10(x3)
U8(x1, x2, x3)  =  U8(x3)
U7(x1, x2, x3)  =  U7(x3)


Using Dependency Pairs [1,30] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

Q_IN(X, f(f(Y))) → U41(X, Y, p_in(X, f(Y)))
Q_IN(X, f(f(Y))) → P_IN(X, f(Y))
P_IN(X, f(Y)) → U61(X, Y, r_in(X, f(Y)))
P_IN(X, f(Y)) → R_IN(X, f(Y))
R_IN(f(X), f(X)) → U111(X, t_in(f(X), f(X)))
R_IN(f(X), f(X)) → T_IN(f(X), f(X))
T_IN(f(X), f(Y)) → U131(X, Y, q_in(f(X), f(Y)))
T_IN(f(X), f(Y)) → Q_IN(f(X), f(Y))
Q_IN(X, f(f(X))) → U21(X, p_in(X, f(f(X))))
Q_IN(X, f(f(X))) → P_IN(X, f(f(X)))
P_IN(X, Y) → U51(X, Y, e_in(X, Y))
P_IN(X, Y) → E_IN(X, Y)
U21(X, p_out(X, f(f(X)))) → U31(X, q_in(X, f(X)))
U21(X, p_out(X, f(f(X)))) → Q_IN(X, f(X))
Q_IN(X, Y) → U11(X, Y, e_in(X, Y))
Q_IN(X, Y) → E_IN(X, Y)
U131(X, Y, q_out(f(X), f(Y))) → U141(X, Y, t_in(X, Y))
U131(X, Y, q_out(f(X), f(Y))) → T_IN(X, Y)
T_IN(X, Y) → U121(X, Y, e_in(X, Y))
T_IN(X, Y) → E_IN(X, Y)
R_IN(X, f(Y)) → U91(X, Y, q_in(X, Y))
R_IN(X, f(Y)) → Q_IN(X, Y)
U91(X, Y, q_out(X, Y)) → U101(X, Y, r_in(X, Y))
U91(X, Y, q_out(X, Y)) → R_IN(X, Y)
R_IN(X, Y) → U81(X, Y, e_in(X, Y))
R_IN(X, Y) → E_IN(X, Y)
U61(X, Y, r_out(X, f(Y))) → U71(X, Y, p_in(X, Y))
U61(X, Y, r_out(X, f(Y))) → P_IN(X, Y)

The TRS R consists of the following rules:

q_in(X, f(f(Y))) → U4(X, Y, p_in(X, f(Y)))
p_in(X, f(Y)) → U6(X, Y, r_in(X, f(Y)))
r_in(f(X), f(X)) → U11(X, t_in(f(X), f(X)))
t_in(f(X), f(Y)) → U13(X, Y, q_in(f(X), f(Y)))
q_in(X, f(f(X))) → U2(X, p_in(X, f(f(X))))
p_in(X, Y) → U5(X, Y, e_in(X, Y))
e_in(a, b) → e_out(a, b)
U5(X, Y, e_out(X, Y)) → p_out(X, Y)
U2(X, p_out(X, f(f(X)))) → U3(X, q_in(X, f(X)))
q_in(X, Y) → U1(X, Y, e_in(X, Y))
U1(X, Y, e_out(X, Y)) → q_out(X, Y)
U3(X, q_out(X, f(X))) → q_out(X, f(f(X)))
U13(X, Y, q_out(f(X), f(Y))) → U14(X, Y, t_in(X, Y))
t_in(X, Y) → U12(X, Y, e_in(X, Y))
U12(X, Y, e_out(X, Y)) → t_out(X, Y)
U14(X, Y, t_out(X, Y)) → t_out(f(X), f(Y))
U11(X, t_out(f(X), f(X))) → r_out(f(X), f(X))
r_in(X, f(Y)) → U9(X, Y, q_in(X, Y))
U9(X, Y, q_out(X, Y)) → U10(X, Y, r_in(X, Y))
r_in(X, Y) → U8(X, Y, e_in(X, Y))
U8(X, Y, e_out(X, Y)) → r_out(X, Y)
U10(X, Y, r_out(X, Y)) → r_out(X, f(Y))
U6(X, Y, r_out(X, f(Y))) → U7(X, Y, p_in(X, Y))
U7(X, Y, p_out(X, Y)) → p_out(X, f(Y))
U4(X, Y, p_out(X, f(Y))) → q_out(X, f(f(Y)))

The argument filtering Pi contains the following mapping:
q_in(x1, x2)  =  q_in(x1, x2)
f(x1)  =  f(x1)
U4(x1, x2, x3)  =  U4(x3)
p_in(x1, x2)  =  p_in(x1, x2)
U6(x1, x2, x3)  =  U6(x1, x2, x3)
r_in(x1, x2)  =  r_in(x1, x2)
U11(x1, x2)  =  U11(x2)
t_in(x1, x2)  =  t_in(x1, x2)
U13(x1, x2, x3)  =  U13(x1, x2, x3)
U2(x1, x2)  =  U2(x1, x2)
U5(x1, x2, x3)  =  U5(x3)
e_in(x1, x2)  =  e_in(x1, x2)
a  =  a
b  =  b
e_out(x1, x2)  =  e_out
p_out(x1, x2)  =  p_out
U3(x1, x2)  =  U3(x2)
U1(x1, x2, x3)  =  U1(x3)
q_out(x1, x2)  =  q_out
U14(x1, x2, x3)  =  U14(x3)
U12(x1, x2, x3)  =  U12(x3)
t_out(x1, x2)  =  t_out
r_out(x1, x2)  =  r_out
U9(x1, x2, x3)  =  U9(x1, x2, x3)
U10(x1, x2, x3)  =  U10(x3)
U8(x1, x2, x3)  =  U8(x3)
U7(x1, x2, x3)  =  U7(x3)
U71(x1, x2, x3)  =  U71(x3)
U51(x1, x2, x3)  =  U51(x3)
U131(x1, x2, x3)  =  U131(x1, x2, x3)
U81(x1, x2, x3)  =  U81(x3)
U31(x1, x2)  =  U31(x2)
U91(x1, x2, x3)  =  U91(x1, x2, x3)
U21(x1, x2)  =  U21(x1, x2)
U11(x1, x2, x3)  =  U11(x3)
P_IN(x1, x2)  =  P_IN(x1, x2)
U111(x1, x2)  =  U111(x2)
U61(x1, x2, x3)  =  U61(x1, x2, x3)
U101(x1, x2, x3)  =  U101(x3)
U41(x1, x2, x3)  =  U41(x3)
T_IN(x1, x2)  =  T_IN(x1, x2)
Q_IN(x1, x2)  =  Q_IN(x1, x2)
U121(x1, x2, x3)  =  U121(x3)
E_IN(x1, x2)  =  E_IN(x1, x2)
U141(x1, x2, x3)  =  U141(x3)
R_IN(x1, x2)  =  R_IN(x1, x2)

We have to consider all (P,R,Pi)-chains

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

Q_IN(X, f(f(Y))) → U41(X, Y, p_in(X, f(Y)))
Q_IN(X, f(f(Y))) → P_IN(X, f(Y))
P_IN(X, f(Y)) → U61(X, Y, r_in(X, f(Y)))
P_IN(X, f(Y)) → R_IN(X, f(Y))
R_IN(f(X), f(X)) → U111(X, t_in(f(X), f(X)))
R_IN(f(X), f(X)) → T_IN(f(X), f(X))
T_IN(f(X), f(Y)) → U131(X, Y, q_in(f(X), f(Y)))
T_IN(f(X), f(Y)) → Q_IN(f(X), f(Y))
Q_IN(X, f(f(X))) → U21(X, p_in(X, f(f(X))))
Q_IN(X, f(f(X))) → P_IN(X, f(f(X)))
P_IN(X, Y) → U51(X, Y, e_in(X, Y))
P_IN(X, Y) → E_IN(X, Y)
U21(X, p_out(X, f(f(X)))) → U31(X, q_in(X, f(X)))
U21(X, p_out(X, f(f(X)))) → Q_IN(X, f(X))
Q_IN(X, Y) → U11(X, Y, e_in(X, Y))
Q_IN(X, Y) → E_IN(X, Y)
U131(X, Y, q_out(f(X), f(Y))) → U141(X, Y, t_in(X, Y))
U131(X, Y, q_out(f(X), f(Y))) → T_IN(X, Y)
T_IN(X, Y) → U121(X, Y, e_in(X, Y))
T_IN(X, Y) → E_IN(X, Y)
R_IN(X, f(Y)) → U91(X, Y, q_in(X, Y))
R_IN(X, f(Y)) → Q_IN(X, Y)
U91(X, Y, q_out(X, Y)) → U101(X, Y, r_in(X, Y))
U91(X, Y, q_out(X, Y)) → R_IN(X, Y)
R_IN(X, Y) → U81(X, Y, e_in(X, Y))
R_IN(X, Y) → E_IN(X, Y)
U61(X, Y, r_out(X, f(Y))) → U71(X, Y, p_in(X, Y))
U61(X, Y, r_out(X, f(Y))) → P_IN(X, Y)

The TRS R consists of the following rules:

q_in(X, f(f(Y))) → U4(X, Y, p_in(X, f(Y)))
p_in(X, f(Y)) → U6(X, Y, r_in(X, f(Y)))
r_in(f(X), f(X)) → U11(X, t_in(f(X), f(X)))
t_in(f(X), f(Y)) → U13(X, Y, q_in(f(X), f(Y)))
q_in(X, f(f(X))) → U2(X, p_in(X, f(f(X))))
p_in(X, Y) → U5(X, Y, e_in(X, Y))
e_in(a, b) → e_out(a, b)
U5(X, Y, e_out(X, Y)) → p_out(X, Y)
U2(X, p_out(X, f(f(X)))) → U3(X, q_in(X, f(X)))
q_in(X, Y) → U1(X, Y, e_in(X, Y))
U1(X, Y, e_out(X, Y)) → q_out(X, Y)
U3(X, q_out(X, f(X))) → q_out(X, f(f(X)))
U13(X, Y, q_out(f(X), f(Y))) → U14(X, Y, t_in(X, Y))
t_in(X, Y) → U12(X, Y, e_in(X, Y))
U12(X, Y, e_out(X, Y)) → t_out(X, Y)
U14(X, Y, t_out(X, Y)) → t_out(f(X), f(Y))
U11(X, t_out(f(X), f(X))) → r_out(f(X), f(X))
r_in(X, f(Y)) → U9(X, Y, q_in(X, Y))
U9(X, Y, q_out(X, Y)) → U10(X, Y, r_in(X, Y))
r_in(X, Y) → U8(X, Y, e_in(X, Y))
U8(X, Y, e_out(X, Y)) → r_out(X, Y)
U10(X, Y, r_out(X, Y)) → r_out(X, f(Y))
U6(X, Y, r_out(X, f(Y))) → U7(X, Y, p_in(X, Y))
U7(X, Y, p_out(X, Y)) → p_out(X, f(Y))
U4(X, Y, p_out(X, f(Y))) → q_out(X, f(f(Y)))

The argument filtering Pi contains the following mapping:
q_in(x1, x2)  =  q_in(x1, x2)
f(x1)  =  f(x1)
U4(x1, x2, x3)  =  U4(x3)
p_in(x1, x2)  =  p_in(x1, x2)
U6(x1, x2, x3)  =  U6(x1, x2, x3)
r_in(x1, x2)  =  r_in(x1, x2)
U11(x1, x2)  =  U11(x2)
t_in(x1, x2)  =  t_in(x1, x2)
U13(x1, x2, x3)  =  U13(x1, x2, x3)
U2(x1, x2)  =  U2(x1, x2)
U5(x1, x2, x3)  =  U5(x3)
e_in(x1, x2)  =  e_in(x1, x2)
a  =  a
b  =  b
e_out(x1, x2)  =  e_out
p_out(x1, x2)  =  p_out
U3(x1, x2)  =  U3(x2)
U1(x1, x2, x3)  =  U1(x3)
q_out(x1, x2)  =  q_out
U14(x1, x2, x3)  =  U14(x3)
U12(x1, x2, x3)  =  U12(x3)
t_out(x1, x2)  =  t_out
r_out(x1, x2)  =  r_out
U9(x1, x2, x3)  =  U9(x1, x2, x3)
U10(x1, x2, x3)  =  U10(x3)
U8(x1, x2, x3)  =  U8(x3)
U7(x1, x2, x3)  =  U7(x3)
U71(x1, x2, x3)  =  U71(x3)
U51(x1, x2, x3)  =  U51(x3)
U131(x1, x2, x3)  =  U131(x1, x2, x3)
U81(x1, x2, x3)  =  U81(x3)
U31(x1, x2)  =  U31(x2)
U91(x1, x2, x3)  =  U91(x1, x2, x3)
U21(x1, x2)  =  U21(x1, x2)
U11(x1, x2, x3)  =  U11(x3)
P_IN(x1, x2)  =  P_IN(x1, x2)
U111(x1, x2)  =  U111(x2)
U61(x1, x2, x3)  =  U61(x1, x2, x3)
U101(x1, x2, x3)  =  U101(x3)
U41(x1, x2, x3)  =  U41(x3)
T_IN(x1, x2)  =  T_IN(x1, x2)
Q_IN(x1, x2)  =  Q_IN(x1, x2)
U121(x1, x2, x3)  =  U121(x3)
E_IN(x1, x2)  =  E_IN(x1, x2)
U141(x1, x2, x3)  =  U141(x3)
R_IN(x1, x2)  =  R_IN(x1, x2)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] contains 1 SCC with 14 less nodes.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

U91(X, Y, q_out(X, Y)) → R_IN(X, Y)
P_IN(X, f(Y)) → R_IN(X, f(Y))
U131(X, Y, q_out(f(X), f(Y))) → T_IN(X, Y)
P_IN(X, f(Y)) → U61(X, Y, r_in(X, f(Y)))
U61(X, Y, r_out(X, f(Y))) → P_IN(X, Y)
R_IN(X, f(Y)) → U91(X, Y, q_in(X, Y))
T_IN(f(X), f(Y)) → Q_IN(f(X), f(Y))
T_IN(f(X), f(Y)) → U131(X, Y, q_in(f(X), f(Y)))
U21(X, p_out(X, f(f(X)))) → Q_IN(X, f(X))
Q_IN(X, f(f(X))) → P_IN(X, f(f(X)))
Q_IN(X, f(f(Y))) → P_IN(X, f(Y))
R_IN(X, f(Y)) → Q_IN(X, Y)
Q_IN(X, f(f(X))) → U21(X, p_in(X, f(f(X))))
R_IN(f(X), f(X)) → T_IN(f(X), f(X))

The TRS R consists of the following rules:

q_in(X, f(f(Y))) → U4(X, Y, p_in(X, f(Y)))
p_in(X, f(Y)) → U6(X, Y, r_in(X, f(Y)))
r_in(f(X), f(X)) → U11(X, t_in(f(X), f(X)))
t_in(f(X), f(Y)) → U13(X, Y, q_in(f(X), f(Y)))
q_in(X, f(f(X))) → U2(X, p_in(X, f(f(X))))
p_in(X, Y) → U5(X, Y, e_in(X, Y))
e_in(a, b) → e_out(a, b)
U5(X, Y, e_out(X, Y)) → p_out(X, Y)
U2(X, p_out(X, f(f(X)))) → U3(X, q_in(X, f(X)))
q_in(X, Y) → U1(X, Y, e_in(X, Y))
U1(X, Y, e_out(X, Y)) → q_out(X, Y)
U3(X, q_out(X, f(X))) → q_out(X, f(f(X)))
U13(X, Y, q_out(f(X), f(Y))) → U14(X, Y, t_in(X, Y))
t_in(X, Y) → U12(X, Y, e_in(X, Y))
U12(X, Y, e_out(X, Y)) → t_out(X, Y)
U14(X, Y, t_out(X, Y)) → t_out(f(X), f(Y))
U11(X, t_out(f(X), f(X))) → r_out(f(X), f(X))
r_in(X, f(Y)) → U9(X, Y, q_in(X, Y))
U9(X, Y, q_out(X, Y)) → U10(X, Y, r_in(X, Y))
r_in(X, Y) → U8(X, Y, e_in(X, Y))
U8(X, Y, e_out(X, Y)) → r_out(X, Y)
U10(X, Y, r_out(X, Y)) → r_out(X, f(Y))
U6(X, Y, r_out(X, f(Y))) → U7(X, Y, p_in(X, Y))
U7(X, Y, p_out(X, Y)) → p_out(X, f(Y))
U4(X, Y, p_out(X, f(Y))) → q_out(X, f(f(Y)))

The argument filtering Pi contains the following mapping:
q_in(x1, x2)  =  q_in(x1, x2)
f(x1)  =  f(x1)
U4(x1, x2, x3)  =  U4(x3)
p_in(x1, x2)  =  p_in(x1, x2)
U6(x1, x2, x3)  =  U6(x1, x2, x3)
r_in(x1, x2)  =  r_in(x1, x2)
U11(x1, x2)  =  U11(x2)
t_in(x1, x2)  =  t_in(x1, x2)
U13(x1, x2, x3)  =  U13(x1, x2, x3)
U2(x1, x2)  =  U2(x1, x2)
U5(x1, x2, x3)  =  U5(x3)
e_in(x1, x2)  =  e_in(x1, x2)
a  =  a
b  =  b
e_out(x1, x2)  =  e_out
p_out(x1, x2)  =  p_out
U3(x1, x2)  =  U3(x2)
U1(x1, x2, x3)  =  U1(x3)
q_out(x1, x2)  =  q_out
U14(x1, x2, x3)  =  U14(x3)
U12(x1, x2, x3)  =  U12(x3)
t_out(x1, x2)  =  t_out
r_out(x1, x2)  =  r_out
U9(x1, x2, x3)  =  U9(x1, x2, x3)
U10(x1, x2, x3)  =  U10(x3)
U8(x1, x2, x3)  =  U8(x3)
U7(x1, x2, x3)  =  U7(x3)
U131(x1, x2, x3)  =  U131(x1, x2, x3)
U91(x1, x2, x3)  =  U91(x1, x2, x3)
U21(x1, x2)  =  U21(x1, x2)
P_IN(x1, x2)  =  P_IN(x1, x2)
U61(x1, x2, x3)  =  U61(x1, x2, x3)
T_IN(x1, x2)  =  T_IN(x1, x2)
Q_IN(x1, x2)  =  Q_IN(x1, x2)
R_IN(x1, x2)  =  R_IN(x1, x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ PiDPToQDPProof
                ↳ QDP
                  ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

P_IN(X, f(Y)) → R_IN(X, f(Y))
P_IN(X, f(Y)) → U61(X, Y, r_in(X, f(Y)))
R_IN(X, f(Y)) → U91(X, Y, q_in(X, Y))
U131(X, Y, q_out) → T_IN(X, Y)
T_IN(f(X), f(Y)) → Q_IN(f(X), f(Y))
U21(X, p_out) → Q_IN(X, f(X))
T_IN(f(X), f(Y)) → U131(X, Y, q_in(f(X), f(Y)))
Q_IN(X, f(f(X))) → P_IN(X, f(f(X)))
U91(X, Y, q_out) → R_IN(X, Y)
Q_IN(X, f(f(Y))) → P_IN(X, f(Y))
U61(X, Y, r_out) → P_IN(X, Y)
R_IN(X, f(Y)) → Q_IN(X, Y)
Q_IN(X, f(f(X))) → U21(X, p_in(X, f(f(X))))
R_IN(f(X), f(X)) → T_IN(f(X), f(X))

The TRS R consists of the following rules:

q_in(X, f(f(Y))) → U4(p_in(X, f(Y)))
p_in(X, f(Y)) → U6(X, Y, r_in(X, f(Y)))
r_in(f(X), f(X)) → U11(t_in(f(X), f(X)))
t_in(f(X), f(Y)) → U13(X, Y, q_in(f(X), f(Y)))
q_in(X, f(f(X))) → U2(X, p_in(X, f(f(X))))
p_in(X, Y) → U5(e_in(X, Y))
e_in(a, b) → e_out
U5(e_out) → p_out
U2(X, p_out) → U3(q_in(X, f(X)))
q_in(X, Y) → U1(e_in(X, Y))
U1(e_out) → q_out
U3(q_out) → q_out
U13(X, Y, q_out) → U14(t_in(X, Y))
t_in(X, Y) → U12(e_in(X, Y))
U12(e_out) → t_out
U14(t_out) → t_out
U11(t_out) → r_out
r_in(X, f(Y)) → U9(X, Y, q_in(X, Y))
U9(X, Y, q_out) → U10(r_in(X, Y))
r_in(X, Y) → U8(e_in(X, Y))
U8(e_out) → r_out
U10(r_out) → r_out
U6(X, Y, r_out) → U7(p_in(X, Y))
U7(p_out) → p_out
U4(p_out) → q_out

The set Q consists of the following terms:

q_in(x0, x1)
p_in(x0, x1)
r_in(x0, x1)
t_in(x0, x1)
e_in(x0, x1)
U5(x0)
U2(x0, x1)
U1(x0)
U3(x0)
U13(x0, x1, x2)
U12(x0)
U14(x0)
U11(x0)
U9(x0, x1, x2)
U8(x0)
U10(x0)
U6(x0, x1, x2)
U7(x0)
U4(x0)

We have to consider all (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


T_IN(f(X), f(Y)) → U131(X, Y, q_in(f(X), f(Y)))
The remaining pairs can at least be oriented weakly.

P_IN(X, f(Y)) → R_IN(X, f(Y))
P_IN(X, f(Y)) → U61(X, Y, r_in(X, f(Y)))
R_IN(X, f(Y)) → U91(X, Y, q_in(X, Y))
U131(X, Y, q_out) → T_IN(X, Y)
T_IN(f(X), f(Y)) → Q_IN(f(X), f(Y))
U21(X, p_out) → Q_IN(X, f(X))
Q_IN(X, f(f(X))) → P_IN(X, f(f(X)))
U91(X, Y, q_out) → R_IN(X, Y)
Q_IN(X, f(f(Y))) → P_IN(X, f(Y))
U61(X, Y, r_out) → P_IN(X, Y)
R_IN(X, f(Y)) → Q_IN(X, Y)
Q_IN(X, f(f(X))) → U21(X, p_in(X, f(f(X))))
R_IN(f(X), f(X)) → T_IN(f(X), f(X))
Used ordering: Polynomial interpretation [25]:

POL(P_IN(x1, x2)) = x1   
POL(Q_IN(x1, x2)) = x1   
POL(R_IN(x1, x2)) = x1   
POL(T_IN(x1, x2)) = x1   
POL(U1(x1)) = 0   
POL(U10(x1)) = 0   
POL(U11(x1)) = 0   
POL(U12(x1)) = 0   
POL(U13(x1, x2, x3)) = 0   
POL(U131(x1, x2, x3)) = x1   
POL(U14(x1)) = 0   
POL(U2(x1, x2)) = 0   
POL(U21(x1, x2)) = x1   
POL(U3(x1)) = 0   
POL(U4(x1)) = 0   
POL(U5(x1)) = 0   
POL(U6(x1, x2, x3)) = 0   
POL(U61(x1, x2, x3)) = x1   
POL(U7(x1)) = 0   
POL(U8(x1)) = 0   
POL(U9(x1, x2, x3)) = 0   
POL(U91(x1, x2, x3)) = x1   
POL(a) = 0   
POL(b) = 1   
POL(e_in(x1, x2)) = x2   
POL(e_out) = 0   
POL(f(x1)) = 1 + x1   
POL(p_in(x1, x2)) = x1 + x2   
POL(p_out) = 0   
POL(q_in(x1, x2)) = 0   
POL(q_out) = 0   
POL(r_in(x1, x2)) = 0   
POL(r_out) = 0   
POL(t_in(x1, x2)) = 0   
POL(t_out) = 0   

The following usable rules [17] were oriented: none



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ PiDPToQDPProof
                ↳ QDP
                  ↳ QDPOrderProof
                    ↳ QDP
                      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

P_IN(X, f(Y)) → R_IN(X, f(Y))
P_IN(X, f(Y)) → U61(X, Y, r_in(X, f(Y)))
R_IN(X, f(Y)) → U91(X, Y, q_in(X, Y))
U131(X, Y, q_out) → T_IN(X, Y)
T_IN(f(X), f(Y)) → Q_IN(f(X), f(Y))
U21(X, p_out) → Q_IN(X, f(X))
Q_IN(X, f(f(X))) → P_IN(X, f(f(X)))
U91(X, Y, q_out) → R_IN(X, Y)
Q_IN(X, f(f(Y))) → P_IN(X, f(Y))
U61(X, Y, r_out) → P_IN(X, Y)
R_IN(X, f(Y)) → Q_IN(X, Y)
Q_IN(X, f(f(X))) → U21(X, p_in(X, f(f(X))))
R_IN(f(X), f(X)) → T_IN(f(X), f(X))

The TRS R consists of the following rules:

q_in(X, f(f(Y))) → U4(p_in(X, f(Y)))
p_in(X, f(Y)) → U6(X, Y, r_in(X, f(Y)))
r_in(f(X), f(X)) → U11(t_in(f(X), f(X)))
t_in(f(X), f(Y)) → U13(X, Y, q_in(f(X), f(Y)))
q_in(X, f(f(X))) → U2(X, p_in(X, f(f(X))))
p_in(X, Y) → U5(e_in(X, Y))
e_in(a, b) → e_out
U5(e_out) → p_out
U2(X, p_out) → U3(q_in(X, f(X)))
q_in(X, Y) → U1(e_in(X, Y))
U1(e_out) → q_out
U3(q_out) → q_out
U13(X, Y, q_out) → U14(t_in(X, Y))
t_in(X, Y) → U12(e_in(X, Y))
U12(e_out) → t_out
U14(t_out) → t_out
U11(t_out) → r_out
r_in(X, f(Y)) → U9(X, Y, q_in(X, Y))
U9(X, Y, q_out) → U10(r_in(X, Y))
r_in(X, Y) → U8(e_in(X, Y))
U8(e_out) → r_out
U10(r_out) → r_out
U6(X, Y, r_out) → U7(p_in(X, Y))
U7(p_out) → p_out
U4(p_out) → q_out

The set Q consists of the following terms:

q_in(x0, x1)
p_in(x0, x1)
r_in(x0, x1)
t_in(x0, x1)
e_in(x0, x1)
U5(x0)
U2(x0, x1)
U1(x0)
U3(x0)
U13(x0, x1, x2)
U12(x0)
U14(x0)
U11(x0)
U9(x0, x1, x2)
U8(x0)
U10(x0)
U6(x0, x1, x2)
U7(x0)
U4(x0)

We have to consider all (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ PiDPToQDPProof
                ↳ QDP
                  ↳ QDPOrderProof
                    ↳ QDP
                      ↳ DependencyGraphProof
                        ↳ QDP
                          ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

U91(X, Y, q_out) → R_IN(X, Y)
P_IN(X, f(Y)) → R_IN(X, f(Y))
Q_IN(X, f(f(Y))) → P_IN(X, f(Y))
P_IN(X, f(Y)) → U61(X, Y, r_in(X, f(Y)))
U61(X, Y, r_out) → P_IN(X, Y)
R_IN(X, f(Y)) → U91(X, Y, q_in(X, Y))
R_IN(X, f(Y)) → Q_IN(X, Y)
Q_IN(X, f(f(X))) → U21(X, p_in(X, f(f(X))))
U21(X, p_out) → Q_IN(X, f(X))
T_IN(f(X), f(Y)) → Q_IN(f(X), f(Y))
R_IN(f(X), f(X)) → T_IN(f(X), f(X))
Q_IN(X, f(f(X))) → P_IN(X, f(f(X)))

The TRS R consists of the following rules:

q_in(X, f(f(Y))) → U4(p_in(X, f(Y)))
p_in(X, f(Y)) → U6(X, Y, r_in(X, f(Y)))
r_in(f(X), f(X)) → U11(t_in(f(X), f(X)))
t_in(f(X), f(Y)) → U13(X, Y, q_in(f(X), f(Y)))
q_in(X, f(f(X))) → U2(X, p_in(X, f(f(X))))
p_in(X, Y) → U5(e_in(X, Y))
e_in(a, b) → e_out
U5(e_out) → p_out
U2(X, p_out) → U3(q_in(X, f(X)))
q_in(X, Y) → U1(e_in(X, Y))
U1(e_out) → q_out
U3(q_out) → q_out
U13(X, Y, q_out) → U14(t_in(X, Y))
t_in(X, Y) → U12(e_in(X, Y))
U12(e_out) → t_out
U14(t_out) → t_out
U11(t_out) → r_out
r_in(X, f(Y)) → U9(X, Y, q_in(X, Y))
U9(X, Y, q_out) → U10(r_in(X, Y))
r_in(X, Y) → U8(e_in(X, Y))
U8(e_out) → r_out
U10(r_out) → r_out
U6(X, Y, r_out) → U7(p_in(X, Y))
U7(p_out) → p_out
U4(p_out) → q_out

The set Q consists of the following terms:

q_in(x0, x1)
p_in(x0, x1)
r_in(x0, x1)
t_in(x0, x1)
e_in(x0, x1)
U5(x0)
U2(x0, x1)
U1(x0)
U3(x0)
U13(x0, x1, x2)
U12(x0)
U14(x0)
U11(x0)
U9(x0, x1, x2)
U8(x0)
U10(x0)
U6(x0, x1, x2)
U7(x0)
U4(x0)

We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule T_IN(f(X), f(Y)) → Q_IN(f(X), f(Y)) we obtained the following new rules:

T_IN(f(z0), f(z0)) → Q_IN(f(z0), f(z0))



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ PiDPToQDPProof
                ↳ QDP
                  ↳ QDPOrderProof
                    ↳ QDP
                      ↳ DependencyGraphProof
                        ↳ QDP
                          ↳ Instantiation
                            ↳ QDP
                              ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

P_IN(X, f(Y)) → R_IN(X, f(Y))
T_IN(f(z0), f(z0)) → Q_IN(f(z0), f(z0))
P_IN(X, f(Y)) → U61(X, Y, r_in(X, f(Y)))
R_IN(X, f(Y)) → U91(X, Y, q_in(X, Y))
U21(X, p_out) → Q_IN(X, f(X))
Q_IN(X, f(f(X))) → P_IN(X, f(f(X)))
U91(X, Y, q_out) → R_IN(X, Y)
Q_IN(X, f(f(Y))) → P_IN(X, f(Y))
U61(X, Y, r_out) → P_IN(X, Y)
R_IN(X, f(Y)) → Q_IN(X, Y)
Q_IN(X, f(f(X))) → U21(X, p_in(X, f(f(X))))
R_IN(f(X), f(X)) → T_IN(f(X), f(X))

The TRS R consists of the following rules:

q_in(X, f(f(Y))) → U4(p_in(X, f(Y)))
p_in(X, f(Y)) → U6(X, Y, r_in(X, f(Y)))
r_in(f(X), f(X)) → U11(t_in(f(X), f(X)))
t_in(f(X), f(Y)) → U13(X, Y, q_in(f(X), f(Y)))
q_in(X, f(f(X))) → U2(X, p_in(X, f(f(X))))
p_in(X, Y) → U5(e_in(X, Y))
e_in(a, b) → e_out
U5(e_out) → p_out
U2(X, p_out) → U3(q_in(X, f(X)))
q_in(X, Y) → U1(e_in(X, Y))
U1(e_out) → q_out
U3(q_out) → q_out
U13(X, Y, q_out) → U14(t_in(X, Y))
t_in(X, Y) → U12(e_in(X, Y))
U12(e_out) → t_out
U14(t_out) → t_out
U11(t_out) → r_out
r_in(X, f(Y)) → U9(X, Y, q_in(X, Y))
U9(X, Y, q_out) → U10(r_in(X, Y))
r_in(X, Y) → U8(e_in(X, Y))
U8(e_out) → r_out
U10(r_out) → r_out
U6(X, Y, r_out) → U7(p_in(X, Y))
U7(p_out) → p_out
U4(p_out) → q_out

The set Q consists of the following terms:

q_in(x0, x1)
p_in(x0, x1)
r_in(x0, x1)
t_in(x0, x1)
e_in(x0, x1)
U5(x0)
U2(x0, x1)
U1(x0)
U3(x0)
U13(x0, x1, x2)
U12(x0)
U14(x0)
U11(x0)
U9(x0, x1, x2)
U8(x0)
U10(x0)
U6(x0, x1, x2)
U7(x0)
U4(x0)

We have to consider all (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


R_IN(X, f(Y)) → U91(X, Y, q_in(X, Y))
Q_IN(X, f(f(Y))) → P_IN(X, f(Y))
U61(X, Y, r_out) → P_IN(X, Y)
R_IN(X, f(Y)) → Q_IN(X, Y)
Q_IN(X, f(f(X))) → U21(X, p_in(X, f(f(X))))
The remaining pairs can at least be oriented weakly.

P_IN(X, f(Y)) → R_IN(X, f(Y))
T_IN(f(z0), f(z0)) → Q_IN(f(z0), f(z0))
P_IN(X, f(Y)) → U61(X, Y, r_in(X, f(Y)))
U21(X, p_out) → Q_IN(X, f(X))
Q_IN(X, f(f(X))) → P_IN(X, f(f(X)))
U91(X, Y, q_out) → R_IN(X, Y)
R_IN(f(X), f(X)) → T_IN(f(X), f(X))
Used ordering: Polynomial interpretation [25]:

POL(P_IN(x1, x2)) = x2   
POL(Q_IN(x1, x2)) = x2   
POL(R_IN(x1, x2)) = x2   
POL(T_IN(x1, x2)) = x1   
POL(U1(x1)) = 0   
POL(U10(x1)) = 0   
POL(U11(x1)) = 0   
POL(U12(x1)) = 1   
POL(U13(x1, x2, x3)) = 0   
POL(U14(x1)) = 0   
POL(U2(x1, x2)) = 0   
POL(U21(x1, x2)) = 1 + x1   
POL(U3(x1)) = 0   
POL(U4(x1)) = 0   
POL(U5(x1)) = 0   
POL(U6(x1, x2, x3)) = 0   
POL(U61(x1, x2, x3)) = 1 + x2   
POL(U7(x1)) = 0   
POL(U8(x1)) = 0   
POL(U9(x1, x2, x3)) = 0   
POL(U91(x1, x2, x3)) = x2   
POL(a) = 0   
POL(b) = 0   
POL(e_in(x1, x2)) = 0   
POL(e_out) = 0   
POL(f(x1)) = 1 + x1   
POL(p_in(x1, x2)) = 0   
POL(p_out) = 0   
POL(q_in(x1, x2)) = 0   
POL(q_out) = 0   
POL(r_in(x1, x2)) = 0   
POL(r_out) = 0   
POL(t_in(x1, x2)) = 1   
POL(t_out) = 0   

The following usable rules [17] were oriented: none



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ PiDPToQDPProof
                ↳ QDP
                  ↳ QDPOrderProof
                    ↳ QDP
                      ↳ DependencyGraphProof
                        ↳ QDP
                          ↳ Instantiation
                            ↳ QDP
                              ↳ QDPOrderProof
                                ↳ QDP
                                  ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

U91(X, Y, q_out) → R_IN(X, Y)
P_IN(X, f(Y)) → R_IN(X, f(Y))
T_IN(f(z0), f(z0)) → Q_IN(f(z0), f(z0))
P_IN(X, f(Y)) → U61(X, Y, r_in(X, f(Y)))
U21(X, p_out) → Q_IN(X, f(X))
R_IN(f(X), f(X)) → T_IN(f(X), f(X))
Q_IN(X, f(f(X))) → P_IN(X, f(f(X)))

The TRS R consists of the following rules:

q_in(X, f(f(Y))) → U4(p_in(X, f(Y)))
p_in(X, f(Y)) → U6(X, Y, r_in(X, f(Y)))
r_in(f(X), f(X)) → U11(t_in(f(X), f(X)))
t_in(f(X), f(Y)) → U13(X, Y, q_in(f(X), f(Y)))
q_in(X, f(f(X))) → U2(X, p_in(X, f(f(X))))
p_in(X, Y) → U5(e_in(X, Y))
e_in(a, b) → e_out
U5(e_out) → p_out
U2(X, p_out) → U3(q_in(X, f(X)))
q_in(X, Y) → U1(e_in(X, Y))
U1(e_out) → q_out
U3(q_out) → q_out
U13(X, Y, q_out) → U14(t_in(X, Y))
t_in(X, Y) → U12(e_in(X, Y))
U12(e_out) → t_out
U14(t_out) → t_out
U11(t_out) → r_out
r_in(X, f(Y)) → U9(X, Y, q_in(X, Y))
U9(X, Y, q_out) → U10(r_in(X, Y))
r_in(X, Y) → U8(e_in(X, Y))
U8(e_out) → r_out
U10(r_out) → r_out
U6(X, Y, r_out) → U7(p_in(X, Y))
U7(p_out) → p_out
U4(p_out) → q_out

The set Q consists of the following terms:

q_in(x0, x1)
p_in(x0, x1)
r_in(x0, x1)
t_in(x0, x1)
e_in(x0, x1)
U5(x0)
U2(x0, x1)
U1(x0)
U3(x0)
U13(x0, x1, x2)
U12(x0)
U14(x0)
U11(x0)
U9(x0, x1, x2)
U8(x0)
U10(x0)
U6(x0, x1, x2)
U7(x0)
U4(x0)

We have to consider all (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 7 less nodes.